YES 11.072000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,r)→r

is transformed to
r0 (_,r) = r

The following Lambda expression
\(n,_)→n

is transformed to
n0 (n,_) = n

The following Lambda expression
\(_,r)→r

is transformed to
r1 (_,r) = r

The following Lambda expression
\(q,_)→q

is transformed to
q1 (q,_) = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if r < 0 then n - 1 else n

is transformed to
floor0 True = n - 1
floor0 False = n

The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
frac@(Double vz wu)

is replaced by the following term
Double vz wu

The bind variable of the following binding Pattern
frac@(Float wx wy)

is replaced by the following term
Float wx wy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
floor0 (r < 0)
where 
floor0 True = n - 1
floor0 False = n
n  = n0 vu9
n0 (n,vw) = n
r  = r0 vu9
r0 (vv,r) = r
vu9  = properFraction x

are unpacked to the following functions on top level
floorN0 xx (n,vw) = n

floorVu9 xx = properFraction xx

floorR xx = floorR0 xx (floorVu9 xx)

floorR0 xx (vv,r) = r

floorN xx = floorN0 xx (floorVu9 xx)

floorFloor0 xx True = floorN xx - 1
floorFloor0 xx False = floorN xx

The bindings of the following Let/Where expression
(fromIntegral q,r :% y)
where 
q  = q1 vu30
q1 (q,xu) = q
r  = r1 vu30
r1 (xv,r) = r
vu30  = quotRem x y

are unpacked to the following functions on top level
properFractionR1 xy xz (xv,r) = r

properFractionQ xy xz = properFractionQ1 xy xz (properFractionVu30 xy xz)

properFractionR xy xz = properFractionR1 xy xz (properFractionVu30 xy xz)

properFractionQ1 xy xz (q,xu) = q

properFractionVu30 xy xz = quotRem xy xz



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((floor :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (floor :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu850)) → new_primMulNat(yu850)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu8000), Succ(yu23300)) → new_primPlusNat(yu8000, yu23300)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yu8000), Succ(yu23300)) → new_primMinusNat(yu8000, yu23300)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS(yu23700000, yu238000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS02(Succ(yu2530), yu254) → new_primModNatS0(yu2530, yu254, yu2530, yu254)
new_primModNatS00(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(Succ(Succ(Zero))), Succ(Succ(Succ(Succ(Succ(yu23800000)))))) → new_primModNatS(Zero, Succ(Succ(Succ(Succ(Succ(yu23800000))))))
new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257))
new_primModNatS1(Succ(yu2370), Zero) → new_primModNatS00(yu2370)
new_primModNatS1(Succ(Succ(Succ(Succ(yu2370000)))), Succ(Succ(Succ(Succ(Zero))))) → new_primModNatS(Succ(yu2370000), Succ(Succ(Succ(Succ(Zero)))))
new_primModNatS1(Succ(Succ(Succ(yu237000))), Succ(Succ(Succ(Zero)))) → new_primModNatS02(yu237000, Succ(Succ(Zero)))
new_primModNatS1(Succ(Succ(yu23700)), Succ(Succ(Zero))) → new_primModNatS02(yu23700, Succ(Zero))
new_primModNatS1(Succ(Succ(Succ(Zero))), Succ(Succ(Succ(Succ(Zero))))) → new_primModNatS(Zero, Succ(Succ(Succ(Succ(Zero)))))
new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257))
new_primModNatS2(Succ(yu2370)) → new_primModNatS00(yu2370)
new_primModNatS1(Succ(yu2370), Succ(Zero)) → new_primModNatS02(yu2370, Zero)
new_primModNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primModNatS0(yu80000, yu81000, yu80000, yu81000)
new_primModNatS1(Succ(Succ(Succ(Succ(yu2370000)))), Succ(Succ(Succ(Succ(Succ(yu23800000)))))) → new_primModNatS(new_primMinusNatS0(yu2370000, yu23800000), Succ(Succ(Succ(Succ(Succ(yu23800000))))))
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS(Succ(Succ(yu80000)), Zero) → new_primModNatS00(yu80000)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 10 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ Rewriting
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257))
new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257))
new_primModNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primModNatS0(yu80000, yu81000, yu80000, yu81000)
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257)) at position [0] we obtained the following new rules:

new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
QDP
                                          ↳ Rewriting
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primModNatS0(yu80000, yu81000, yu80000, yu81000)
new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(Succ(yu256), Succ(yu257)), Succ(yu257)) at position [0] we obtained the following new rules:

new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
QDP
                                              ↳ QDPOrderProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primModNatS0(yu80000, yu81000, yu80000, yu81000)
new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primModNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primModNatS0(yu80000, yu81000, yu80000, yu81000)
The remaining pairs can at least be oriented weakly.

new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primMinusNatS0(x1, x2)) = x1   
POL(new_primModNatS(x1, x2)) = x1   
POL(new_primModNatS0(x1, x2, x3, x4)) = x1   
POL(new_primModNatS01(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
QDP
                                                  ↳ DependencyGraphProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS01(yu256, yu257) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Zero) → new_primModNatS(new_primMinusNatS0(yu256, yu257), Succ(yu257))
new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)
new_primModNatS0(yu256, yu257, Zero, Zero) → new_primModNatS01(yu256, yu257)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
QDP
                                                      ↳ UsableRulesProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
QDP
                                                          ↳ QReductionProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
                                                        ↳ QDP
                                                          ↳ QReductionProof
QDP
                                                              ↳ QDPSizeChangeProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(yu256, yu257, Succ(yu2580), Succ(yu2590)) → new_primModNatS0(yu256, yu257, yu2580, yu2590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu2370), Zero) → new_primModNatS00(yu2370)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ UsableRulesProof
QDP
                                          ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu2370), Zero) → new_primModNatS00(yu2370)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ UsableRulesProof
                                        ↳ QDP
                                          ↳ QReductionProof
QDP
                                              ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu2370), Zero) → new_primModNatS00(yu2370)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277))
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277))
new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS01
new_primDivNatS01new_primDivNatS(Zero, Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ UsableRulesProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
QDP
                                          ↳ RuleRemovalProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 2 + 2·x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1 + x2   
POL(new_primMinusNatS0(x1, x2)) = 1 + 2·x1 + x2   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
                                        ↳ QDP
                                          ↳ RuleRemovalProof
QDP
                                              ↳ PisEmptyProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ Rewriting
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277))
new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277)) at position [0] we obtained the following new rules:

new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
QDP
                                          ↳ Rewriting
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu276), Succ(yu277)), Succ(yu277)) at position [0] we obtained the following new rules:

new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
QDP
                                              ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
The remaining pairs can at least be oriented weakly.

new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1   
POL(new_primDivNatS0(x1, x2, x3, x4)) = x1   
POL(new_primDivNatS00(x1, x2)) = x1   
POL(new_primMinusNatS0(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
QDP
                                                  ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Zero, Zero) → new_primDivNatS00(yu276, yu277)
new_primDivNatS00(yu276, yu277) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))
new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)
new_primDivNatS0(yu276, yu277, Succ(yu2780), Zero) → new_primDivNatS(new_primMinusNatS0(yu276, yu277), Succ(yu277))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
QDP
                                                      ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu238000000)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu23700000), Succ(yu238000000)) → new_primMinusNatS0(yu23700000, yu238000000)
new_primMinusNatS0(Succ(yu23700000), Zero) → Succ(yu23700000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
QDP
                                                          ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
                                                        ↳ QDP
                                                          ↳ QReductionProof
QDP
                                                              ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu276, yu277, Succ(yu2780), Succ(yu2790)) → new_primDivNatS0(yu276, yu277, yu2780, yu2790)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_floorFloor0(yu30000000, Succ(yu20900), Succ(yu10200)) → new_floorFloor0(yu30000000, yu20900, yu10200)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_floorFloor00(yu30000000, Succ(yu13300), Succ(yu20500)) → new_floorFloor00(yu30000000, yu13300, yu20500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: